(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 5))
(declare-fun v1 () (_ BitVec 4))
(assert (let ((e2(_ bv12 5)))
(let ((e3 (bvneg v0)))
(let ((e4 ((_ rotate_right 0) e2)))
(let ((e5 (bvsub e2 e2)))
(let ((e6 (concat e5 e3)))
(let ((e7 (ite (= (_ bv1 1) ((_ extract 4 4) v0)) e2 e2)))
(let ((e8 (bvsrem ((_ sign_extend 5) v0) e6)))
(let ((e9 (bvadd ((_ zero_extend 5) e3) e8)))
(let ((e10 (ite (bvsgt e6 e6) (_ bv1 1) (_ bv0 1))))
(let ((e11 (bvmul ((_ zero_extend 5) v0) e9)))
(let ((e12 (bvmul e9 e11)))
(let ((e13 (bvxnor ((_ zero_extend 5) e2) e12)))
(let ((e14 (ite (bvuge e3 e2) (_ bv1 1) (_ bv0 1))))
(let ((e15 (bvashr e2 e3)))
(let ((e16 (bvashr e11 ((_ sign_extend 6) v1))))
(let ((e17 (= e6 ((_ zero_extend 9) e10))))
(let ((e18 (bvsle e16 ((_ sign_extend 6) v1))))
(let ((e19 (bvult ((_ sign_extend 5) e5) e13)))
(let ((e20 (= e5 ((_ zero_extend 1) v1))))
(let ((e21 (= e5 e5)))
(let ((e22 (= ((_ sign_extend 4) e14) v0)))
(let ((e23 (distinct e16 e13)))
(let ((e24 (bvslt ((_ zero_extend 5) e3) e6)))
(let ((e25 (bvule e6 ((_ zero_extend 5) e2))))
(let ((e26 (bvslt ((_ sign_extend 5) e2) e11)))
(let ((e27 (bvslt e7 e5)))
(let ((e28 (= ((_ sign_extend 5) v0) e6)))
(let ((e29 (distinct ((_ zero_extend 5) e7) e8)))
(let ((e30 (bvugt e6 ((_ sign_extend 6) v1))))
(let ((e31 (= e4 e4)))
(let ((e32 (bvule ((_ sign_extend 5) e3) e16)))
(let ((e33 (bvsge e8 e11)))
(let ((e34 (bvult ((_ sign_extend 4) e14) e4)))
(let ((e35 (bvuge v0 v0)))
(let ((e36 (bvugt e8 e8)))
(let ((e37 (bvule ((_ zero_extend 6) v1) e12)))
(let ((e38 (bvsle e11 ((_ zero_extend 9) e14))))
(let ((e39 (bvsle ((_ zero_extend 5) e15) e6)))
(let ((e40 (= ((_ sign_extend 5) v0) e16)))
(let ((e41 (bvugt ((_ sign_extend 4) e10) e4)))
(let ((e42 (bvsle e13 e6)))
(let ((e43 (distinct e8 ((_ zero_extend 9) e10))))
(let ((e44 (bvsge ((_ zero_extend 5) v0) e6)))
(let ((e45 (bvugt e16 ((_ sign_extend 5) e7))))
(let ((e46 (bvule ((_ sign_extend 9) e10) e6)))
(let ((e47 (bvugt e2 e15)))
(let ((e48 (bvsge e16 ((_ zero_extend 5) e4))))
(let ((e49 (= e8 e8)))
(let ((e50 (bvsgt e12 ((_ sign_extend 5) e15))))
(let ((e51 (bvsle e8 e12)))
(let ((e52 (= e6 ((_ sign_extend 5) e7))))
(let ((e53 (bvslt ((_ sign_extend 5) v0) e9)))
(let ((e54 (= e53 e46)))
(let ((e55 (xor e33 e29)))
(let ((e56 (xor e48 e27)))
(let ((e57 (=> e54 e52)))
(let ((e58 (or e44 e51)))
(let ((e59 (not e37)))
(let ((e60 (or e26 e56)))
(let ((e61 (not e30)))
(let ((e62 (xor e43 e59)))
(let ((e63 (and e20 e49)))
(let ((e64 (= e23 e45)))
(let ((e65 (and e58 e22)))
(let ((e66 (ite e41 e42 e61)))
(let ((e67 (ite e39 e24 e21)))
(let ((e68 (and e67 e32)))
(let ((e69 (ite e35 e35 e35)))
(let ((e70 (xor e31 e63)))
(let ((e71 (=> e25 e18)))
(let ((e72 (xor e68 e17)))
(let ((e73 (ite e62 e36 e64)))
(let ((e74 (= e69 e50)))
(let ((e75 (xor e47 e34)))
(let ((e76 (not e38)))
(let ((e77 (and e19 e74)))
(let ((e78 (or e60 e40)))
(let ((e79 (or e73 e78)))
(let ((e80 (or e77 e76)))
(let ((e81 (not e70)))
(let ((e82 (and e80 e72)))
(let ((e83 (=> e55 e81)))
(let ((e84 (=> e28 e71)))
(let ((e85 (=> e79 e75)))
(let ((e86 (= e82 e82)))
(let ((e87 (ite e84 e66 e66)))
(let ((e88 (xor e87 e83)))
(let ((e89 (and e85 e86)))
(let ((e90 (ite e88 e57 e57)))
(let ((e91 (= e90 e90)))
(let ((e92 (and e91 e65)))
(let ((e93 (=> e89 e89)))
(let ((e94 (and e92 e92)))
(let ((e95 (not e94)))
(let ((e96 (=> e93 e95)))
(let ((e97 (and e96 (not (= e6 (_ bv0 10))))))
(let ((e98 (and e97 (not (= e6 (bvnot (_ bv0 10)))))))
e98
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
